
# Chalice - Verification of Concurrent Software

Chalice is both a research programming language as well as a verification tool
for that language.  The language is a simple, object-based programming
language with support for thread-based concurrency using fork/join as well as
monitors and channels.  Chalice allows programmers to make assumptions explicit
using specifications such as pre/postconditions as well invariants which are
then checked for correctness.

Chalice is implemented in Scala and builds on top of the intermediate
verification language Boogie, which in turn is based on the SMT solver Z3.


## Prerequisites

Chalice is developed and tested on Windows.  It may be possible to run it on
other operating systems, but not all scripts are available for other operation
systems.

Before Chalice can be used successfully, Boogie and Z3 need to be installed

- Boogie is available for download at http://boogie.codeplex.com/.  By default,
  Chalice expects Boogie to be located at `C:\binaries\boogie\boogie.exe`.  It
  is also possible to specify the path to Boogie manually using the command-line
  argument `/boogie:<path>`

- Z3 is available at http://z3.codeplex.com/.  Boogie recognizes the default
  installation location when a version of Z3 is used that comes with an
  installer, and checks the PATH environment variable.  It is also possible to
  specify the location of the Z3 executable manually using the Chalice
  command-line argument `/boogieOpt:"z3exe:<path>"`.

It is possible to change the file `chalice.bat` to include the arguments to set
the paths to Boogie and Z3, such that these don't have to be provided every
time.


## Using Chalice

Chalice is a command-line tool that can be invoked using the script
`chalice.bat`.  In its simplest form, Chalice requires only a path to a file
containing a Chalice program.  For instance:
    chalice.bat test/examples/CopyLessMessagePassing.chalice

For more information on available command line parameters, we refer to

    chalice.bat /help


## Building Chalice from Source

Chalice is build using sbt, whose binary is included in the Chalice repository.
Compiling Chalice is thus done using

    sbt compile

The tests that come with Chalice can be executed using various scripts located
in the directory `tests`.  For more information on the tests, see
`tests/readme.txt`.
